active(__(__(X, Y), Z)) → mark(__(X, __(Y, Z)))
active(__(X, nil)) → mark(X)
active(__(nil, X)) → mark(X)
active(and(tt, X)) → mark(X)
active(isNePal(__(I, __(P, I)))) → mark(tt)
active(__(X1, X2)) → __(active(X1), X2)
active(__(X1, X2)) → __(X1, active(X2))
active(and(X1, X2)) → and(active(X1), X2)
active(isNePal(X)) → isNePal(active(X))
__(mark(X1), X2) → mark(__(X1, X2))
__(X1, mark(X2)) → mark(__(X1, X2))
and(mark(X1), X2) → mark(and(X1, X2))
isNePal(mark(X)) → mark(isNePal(X))
proper(__(X1, X2)) → __(proper(X1), proper(X2))
proper(nil) → ok(nil)
proper(and(X1, X2)) → and(proper(X1), proper(X2))
proper(tt) → ok(tt)
proper(isNePal(X)) → isNePal(proper(X))
__(ok(X1), ok(X2)) → ok(__(X1, X2))
and(ok(X1), ok(X2)) → ok(and(X1, X2))
isNePal(ok(X)) → ok(isNePal(X))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))
↳ QTRS
↳ DependencyPairsProof
active(__(__(X, Y), Z)) → mark(__(X, __(Y, Z)))
active(__(X, nil)) → mark(X)
active(__(nil, X)) → mark(X)
active(and(tt, X)) → mark(X)
active(isNePal(__(I, __(P, I)))) → mark(tt)
active(__(X1, X2)) → __(active(X1), X2)
active(__(X1, X2)) → __(X1, active(X2))
active(and(X1, X2)) → and(active(X1), X2)
active(isNePal(X)) → isNePal(active(X))
__(mark(X1), X2) → mark(__(X1, X2))
__(X1, mark(X2)) → mark(__(X1, X2))
and(mark(X1), X2) → mark(and(X1, X2))
isNePal(mark(X)) → mark(isNePal(X))
proper(__(X1, X2)) → __(proper(X1), proper(X2))
proper(nil) → ok(nil)
proper(and(X1, X2)) → and(proper(X1), proper(X2))
proper(tt) → ok(tt)
proper(isNePal(X)) → isNePal(proper(X))
__(ok(X1), ok(X2)) → ok(__(X1, X2))
and(ok(X1), ok(X2)) → ok(and(X1, X2))
isNePal(ok(X)) → ok(isNePal(X))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))
ISNEPAL(mark(X)) → ISNEPAL(X)
TOP(mark(X)) → PROPER(X)
PROPER(__(X1, X2)) → PROPER(X2)
ACTIVE(isNePal(X)) → ACTIVE(X)
PROPER(__(X1, X2)) → __1(proper(X1), proper(X2))
ACTIVE(and(X1, X2)) → AND(active(X1), X2)
AND(ok(X1), ok(X2)) → AND(X1, X2)
TOP(ok(X)) → ACTIVE(X)
PROPER(and(X1, X2)) → AND(proper(X1), proper(X2))
PROPER(isNePal(X)) → PROPER(X)
ACTIVE(isNePal(X)) → ISNEPAL(active(X))
PROPER(__(X1, X2)) → PROPER(X1)
ACTIVE(__(X1, X2)) → ACTIVE(X2)
ISNEPAL(ok(X)) → ISNEPAL(X)
TOP(ok(X)) → TOP(active(X))
PROPER(isNePal(X)) → ISNEPAL(proper(X))
PROPER(and(X1, X2)) → PROPER(X1)
ACTIVE(__(__(X, Y), Z)) → __1(X, __(Y, Z))
__1(X1, mark(X2)) → __1(X1, X2)
ACTIVE(and(X1, X2)) → ACTIVE(X1)
ACTIVE(__(X1, X2)) → ACTIVE(X1)
PROPER(and(X1, X2)) → PROPER(X2)
AND(mark(X1), X2) → AND(X1, X2)
ACTIVE(__(__(X, Y), Z)) → __1(Y, Z)
TOP(mark(X)) → TOP(proper(X))
__1(ok(X1), ok(X2)) → __1(X1, X2)
__1(mark(X1), X2) → __1(X1, X2)
ACTIVE(__(X1, X2)) → __1(active(X1), X2)
ACTIVE(__(X1, X2)) → __1(X1, active(X2))
active(__(__(X, Y), Z)) → mark(__(X, __(Y, Z)))
active(__(X, nil)) → mark(X)
active(__(nil, X)) → mark(X)
active(and(tt, X)) → mark(X)
active(isNePal(__(I, __(P, I)))) → mark(tt)
active(__(X1, X2)) → __(active(X1), X2)
active(__(X1, X2)) → __(X1, active(X2))
active(and(X1, X2)) → and(active(X1), X2)
active(isNePal(X)) → isNePal(active(X))
__(mark(X1), X2) → mark(__(X1, X2))
__(X1, mark(X2)) → mark(__(X1, X2))
and(mark(X1), X2) → mark(and(X1, X2))
isNePal(mark(X)) → mark(isNePal(X))
proper(__(X1, X2)) → __(proper(X1), proper(X2))
proper(nil) → ok(nil)
proper(and(X1, X2)) → and(proper(X1), proper(X2))
proper(tt) → ok(tt)
proper(isNePal(X)) → isNePal(proper(X))
__(ok(X1), ok(X2)) → ok(__(X1, X2))
and(ok(X1), ok(X2)) → ok(and(X1, X2))
isNePal(ok(X)) → ok(isNePal(X))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
ISNEPAL(mark(X)) → ISNEPAL(X)
TOP(mark(X)) → PROPER(X)
PROPER(__(X1, X2)) → PROPER(X2)
ACTIVE(isNePal(X)) → ACTIVE(X)
PROPER(__(X1, X2)) → __1(proper(X1), proper(X2))
ACTIVE(and(X1, X2)) → AND(active(X1), X2)
AND(ok(X1), ok(X2)) → AND(X1, X2)
TOP(ok(X)) → ACTIVE(X)
PROPER(and(X1, X2)) → AND(proper(X1), proper(X2))
PROPER(isNePal(X)) → PROPER(X)
ACTIVE(isNePal(X)) → ISNEPAL(active(X))
PROPER(__(X1, X2)) → PROPER(X1)
ACTIVE(__(X1, X2)) → ACTIVE(X2)
ISNEPAL(ok(X)) → ISNEPAL(X)
TOP(ok(X)) → TOP(active(X))
PROPER(isNePal(X)) → ISNEPAL(proper(X))
PROPER(and(X1, X2)) → PROPER(X1)
ACTIVE(__(__(X, Y), Z)) → __1(X, __(Y, Z))
__1(X1, mark(X2)) → __1(X1, X2)
ACTIVE(and(X1, X2)) → ACTIVE(X1)
ACTIVE(__(X1, X2)) → ACTIVE(X1)
PROPER(and(X1, X2)) → PROPER(X2)
AND(mark(X1), X2) → AND(X1, X2)
ACTIVE(__(__(X, Y), Z)) → __1(Y, Z)
TOP(mark(X)) → TOP(proper(X))
__1(ok(X1), ok(X2)) → __1(X1, X2)
__1(mark(X1), X2) → __1(X1, X2)
ACTIVE(__(X1, X2)) → __1(active(X1), X2)
ACTIVE(__(X1, X2)) → __1(X1, active(X2))
active(__(__(X, Y), Z)) → mark(__(X, __(Y, Z)))
active(__(X, nil)) → mark(X)
active(__(nil, X)) → mark(X)
active(and(tt, X)) → mark(X)
active(isNePal(__(I, __(P, I)))) → mark(tt)
active(__(X1, X2)) → __(active(X1), X2)
active(__(X1, X2)) → __(X1, active(X2))
active(and(X1, X2)) → and(active(X1), X2)
active(isNePal(X)) → isNePal(active(X))
__(mark(X1), X2) → mark(__(X1, X2))
__(X1, mark(X2)) → mark(__(X1, X2))
and(mark(X1), X2) → mark(and(X1, X2))
isNePal(mark(X)) → mark(isNePal(X))
proper(__(X1, X2)) → __(proper(X1), proper(X2))
proper(nil) → ok(nil)
proper(and(X1, X2)) → and(proper(X1), proper(X2))
proper(tt) → ok(tt)
proper(isNePal(X)) → isNePal(proper(X))
__(ok(X1), ok(X2)) → ok(__(X1, X2))
and(ok(X1), ok(X2)) → ok(and(X1, X2))
isNePal(ok(X)) → ok(isNePal(X))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
ISNEPAL(mark(X)) → ISNEPAL(X)
ISNEPAL(ok(X)) → ISNEPAL(X)
active(__(__(X, Y), Z)) → mark(__(X, __(Y, Z)))
active(__(X, nil)) → mark(X)
active(__(nil, X)) → mark(X)
active(and(tt, X)) → mark(X)
active(isNePal(__(I, __(P, I)))) → mark(tt)
active(__(X1, X2)) → __(active(X1), X2)
active(__(X1, X2)) → __(X1, active(X2))
active(and(X1, X2)) → and(active(X1), X2)
active(isNePal(X)) → isNePal(active(X))
__(mark(X1), X2) → mark(__(X1, X2))
__(X1, mark(X2)) → mark(__(X1, X2))
and(mark(X1), X2) → mark(and(X1, X2))
isNePal(mark(X)) → mark(isNePal(X))
proper(__(X1, X2)) → __(proper(X1), proper(X2))
proper(nil) → ok(nil)
proper(and(X1, X2)) → and(proper(X1), proper(X2))
proper(tt) → ok(tt)
proper(isNePal(X)) → isNePal(proper(X))
__(ok(X1), ok(X2)) → ok(__(X1, X2))
and(ok(X1), ok(X2)) → ok(and(X1, X2))
isNePal(ok(X)) → ok(isNePal(X))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
ISNEPAL(mark(X)) → ISNEPAL(X)
ISNEPAL(ok(X)) → ISNEPAL(X)
The value of delta used in the strict ordering is 16.
POL(mark(x1)) = 4 + (4)x_1
POL(ok(x1)) = 4 + x_1
POL(ISNEPAL(x1)) = (4)x_1
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
active(__(__(X, Y), Z)) → mark(__(X, __(Y, Z)))
active(__(X, nil)) → mark(X)
active(__(nil, X)) → mark(X)
active(and(tt, X)) → mark(X)
active(isNePal(__(I, __(P, I)))) → mark(tt)
active(__(X1, X2)) → __(active(X1), X2)
active(__(X1, X2)) → __(X1, active(X2))
active(and(X1, X2)) → and(active(X1), X2)
active(isNePal(X)) → isNePal(active(X))
__(mark(X1), X2) → mark(__(X1, X2))
__(X1, mark(X2)) → mark(__(X1, X2))
and(mark(X1), X2) → mark(and(X1, X2))
isNePal(mark(X)) → mark(isNePal(X))
proper(__(X1, X2)) → __(proper(X1), proper(X2))
proper(nil) → ok(nil)
proper(and(X1, X2)) → and(proper(X1), proper(X2))
proper(tt) → ok(tt)
proper(isNePal(X)) → isNePal(proper(X))
__(ok(X1), ok(X2)) → ok(__(X1, X2))
and(ok(X1), ok(X2)) → ok(and(X1, X2))
isNePal(ok(X)) → ok(isNePal(X))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
AND(mark(X1), X2) → AND(X1, X2)
AND(ok(X1), ok(X2)) → AND(X1, X2)
active(__(__(X, Y), Z)) → mark(__(X, __(Y, Z)))
active(__(X, nil)) → mark(X)
active(__(nil, X)) → mark(X)
active(and(tt, X)) → mark(X)
active(isNePal(__(I, __(P, I)))) → mark(tt)
active(__(X1, X2)) → __(active(X1), X2)
active(__(X1, X2)) → __(X1, active(X2))
active(and(X1, X2)) → and(active(X1), X2)
active(isNePal(X)) → isNePal(active(X))
__(mark(X1), X2) → mark(__(X1, X2))
__(X1, mark(X2)) → mark(__(X1, X2))
and(mark(X1), X2) → mark(and(X1, X2))
isNePal(mark(X)) → mark(isNePal(X))
proper(__(X1, X2)) → __(proper(X1), proper(X2))
proper(nil) → ok(nil)
proper(and(X1, X2)) → and(proper(X1), proper(X2))
proper(tt) → ok(tt)
proper(isNePal(X)) → isNePal(proper(X))
__(ok(X1), ok(X2)) → ok(__(X1, X2))
and(ok(X1), ok(X2)) → ok(and(X1, X2))
isNePal(ok(X)) → ok(isNePal(X))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
AND(mark(X1), X2) → AND(X1, X2)
AND(ok(X1), ok(X2)) → AND(X1, X2)
The value of delta used in the strict ordering is 5.
POL(AND(x1, x2)) = (4)x_1 + x_2
POL(mark(x1)) = 4 + (2)x_1
POL(ok(x1)) = 1 + (4)x_1
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
active(__(__(X, Y), Z)) → mark(__(X, __(Y, Z)))
active(__(X, nil)) → mark(X)
active(__(nil, X)) → mark(X)
active(and(tt, X)) → mark(X)
active(isNePal(__(I, __(P, I)))) → mark(tt)
active(__(X1, X2)) → __(active(X1), X2)
active(__(X1, X2)) → __(X1, active(X2))
active(and(X1, X2)) → and(active(X1), X2)
active(isNePal(X)) → isNePal(active(X))
__(mark(X1), X2) → mark(__(X1, X2))
__(X1, mark(X2)) → mark(__(X1, X2))
and(mark(X1), X2) → mark(and(X1, X2))
isNePal(mark(X)) → mark(isNePal(X))
proper(__(X1, X2)) → __(proper(X1), proper(X2))
proper(nil) → ok(nil)
proper(and(X1, X2)) → and(proper(X1), proper(X2))
proper(tt) → ok(tt)
proper(isNePal(X)) → isNePal(proper(X))
__(ok(X1), ok(X2)) → ok(__(X1, X2))
and(ok(X1), ok(X2)) → ok(and(X1, X2))
isNePal(ok(X)) → ok(isNePal(X))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDP
↳ QDP
__1(ok(X1), ok(X2)) → __1(X1, X2)
__1(X1, mark(X2)) → __1(X1, X2)
__1(mark(X1), X2) → __1(X1, X2)
active(__(__(X, Y), Z)) → mark(__(X, __(Y, Z)))
active(__(X, nil)) → mark(X)
active(__(nil, X)) → mark(X)
active(and(tt, X)) → mark(X)
active(isNePal(__(I, __(P, I)))) → mark(tt)
active(__(X1, X2)) → __(active(X1), X2)
active(__(X1, X2)) → __(X1, active(X2))
active(and(X1, X2)) → and(active(X1), X2)
active(isNePal(X)) → isNePal(active(X))
__(mark(X1), X2) → mark(__(X1, X2))
__(X1, mark(X2)) → mark(__(X1, X2))
and(mark(X1), X2) → mark(and(X1, X2))
isNePal(mark(X)) → mark(isNePal(X))
proper(__(X1, X2)) → __(proper(X1), proper(X2))
proper(nil) → ok(nil)
proper(and(X1, X2)) → and(proper(X1), proper(X2))
proper(tt) → ok(tt)
proper(isNePal(X)) → isNePal(proper(X))
__(ok(X1), ok(X2)) → ok(__(X1, X2))
and(ok(X1), ok(X2)) → ok(and(X1, X2))
isNePal(ok(X)) → ok(isNePal(X))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
__1(ok(X1), ok(X2)) → __1(X1, X2)
__1(X1, mark(X2)) → __1(X1, X2)
__1(mark(X1), X2) → __1(X1, X2)
The value of delta used in the strict ordering is 16.
POL(__1(x1, x2)) = (4)x_1 + (4)x_2
POL(ok(x1)) = 4 + (2)x_1
POL(mark(x1)) = 4 + (2)x_1
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
↳ QDP
↳ QDP
↳ QDP
active(__(__(X, Y), Z)) → mark(__(X, __(Y, Z)))
active(__(X, nil)) → mark(X)
active(__(nil, X)) → mark(X)
active(and(tt, X)) → mark(X)
active(isNePal(__(I, __(P, I)))) → mark(tt)
active(__(X1, X2)) → __(active(X1), X2)
active(__(X1, X2)) → __(X1, active(X2))
active(and(X1, X2)) → and(active(X1), X2)
active(isNePal(X)) → isNePal(active(X))
__(mark(X1), X2) → mark(__(X1, X2))
__(X1, mark(X2)) → mark(__(X1, X2))
and(mark(X1), X2) → mark(and(X1, X2))
isNePal(mark(X)) → mark(isNePal(X))
proper(__(X1, X2)) → __(proper(X1), proper(X2))
proper(nil) → ok(nil)
proper(and(X1, X2)) → and(proper(X1), proper(X2))
proper(tt) → ok(tt)
proper(isNePal(X)) → isNePal(proper(X))
__(ok(X1), ok(X2)) → ok(__(X1, X2))
and(ok(X1), ok(X2)) → ok(and(X1, X2))
isNePal(ok(X)) → ok(isNePal(X))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDP
PROPER(and(X1, X2)) → PROPER(X2)
PROPER(isNePal(X)) → PROPER(X)
PROPER(and(X1, X2)) → PROPER(X1)
PROPER(__(X1, X2)) → PROPER(X2)
PROPER(__(X1, X2)) → PROPER(X1)
active(__(__(X, Y), Z)) → mark(__(X, __(Y, Z)))
active(__(X, nil)) → mark(X)
active(__(nil, X)) → mark(X)
active(and(tt, X)) → mark(X)
active(isNePal(__(I, __(P, I)))) → mark(tt)
active(__(X1, X2)) → __(active(X1), X2)
active(__(X1, X2)) → __(X1, active(X2))
active(and(X1, X2)) → and(active(X1), X2)
active(isNePal(X)) → isNePal(active(X))
__(mark(X1), X2) → mark(__(X1, X2))
__(X1, mark(X2)) → mark(__(X1, X2))
and(mark(X1), X2) → mark(and(X1, X2))
isNePal(mark(X)) → mark(isNePal(X))
proper(__(X1, X2)) → __(proper(X1), proper(X2))
proper(nil) → ok(nil)
proper(and(X1, X2)) → and(proper(X1), proper(X2))
proper(tt) → ok(tt)
proper(isNePal(X)) → isNePal(proper(X))
__(ok(X1), ok(X2)) → ok(__(X1, X2))
and(ok(X1), ok(X2)) → ok(and(X1, X2))
isNePal(ok(X)) → ok(isNePal(X))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
PROPER(and(X1, X2)) → PROPER(X2)
PROPER(isNePal(X)) → PROPER(X)
PROPER(and(X1, X2)) → PROPER(X1)
PROPER(__(X1, X2)) → PROPER(X2)
PROPER(__(X1, X2)) → PROPER(X1)
The value of delta used in the strict ordering is 16.
POL(PROPER(x1)) = (4)x_1
POL(__(x1, x2)) = 4 + (4)x_1 + (2)x_2
POL(isNePal(x1)) = 4 + (4)x_1
POL(and(x1, x2)) = 4 + (2)x_1 + (3)x_2
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
↳ QDP
↳ QDP
active(__(__(X, Y), Z)) → mark(__(X, __(Y, Z)))
active(__(X, nil)) → mark(X)
active(__(nil, X)) → mark(X)
active(and(tt, X)) → mark(X)
active(isNePal(__(I, __(P, I)))) → mark(tt)
active(__(X1, X2)) → __(active(X1), X2)
active(__(X1, X2)) → __(X1, active(X2))
active(and(X1, X2)) → and(active(X1), X2)
active(isNePal(X)) → isNePal(active(X))
__(mark(X1), X2) → mark(__(X1, X2))
__(X1, mark(X2)) → mark(__(X1, X2))
and(mark(X1), X2) → mark(and(X1, X2))
isNePal(mark(X)) → mark(isNePal(X))
proper(__(X1, X2)) → __(proper(X1), proper(X2))
proper(nil) → ok(nil)
proper(and(X1, X2)) → and(proper(X1), proper(X2))
proper(tt) → ok(tt)
proper(isNePal(X)) → isNePal(proper(X))
__(ok(X1), ok(X2)) → ok(__(X1, X2))
and(ok(X1), ok(X2)) → ok(and(X1, X2))
isNePal(ok(X)) → ok(isNePal(X))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
ACTIVE(isNePal(X)) → ACTIVE(X)
ACTIVE(and(X1, X2)) → ACTIVE(X1)
ACTIVE(__(X1, X2)) → ACTIVE(X2)
ACTIVE(__(X1, X2)) → ACTIVE(X1)
active(__(__(X, Y), Z)) → mark(__(X, __(Y, Z)))
active(__(X, nil)) → mark(X)
active(__(nil, X)) → mark(X)
active(and(tt, X)) → mark(X)
active(isNePal(__(I, __(P, I)))) → mark(tt)
active(__(X1, X2)) → __(active(X1), X2)
active(__(X1, X2)) → __(X1, active(X2))
active(and(X1, X2)) → and(active(X1), X2)
active(isNePal(X)) → isNePal(active(X))
__(mark(X1), X2) → mark(__(X1, X2))
__(X1, mark(X2)) → mark(__(X1, X2))
and(mark(X1), X2) → mark(and(X1, X2))
isNePal(mark(X)) → mark(isNePal(X))
proper(__(X1, X2)) → __(proper(X1), proper(X2))
proper(nil) → ok(nil)
proper(and(X1, X2)) → and(proper(X1), proper(X2))
proper(tt) → ok(tt)
proper(isNePal(X)) → isNePal(proper(X))
__(ok(X1), ok(X2)) → ok(__(X1, X2))
and(ok(X1), ok(X2)) → ok(and(X1, X2))
isNePal(ok(X)) → ok(isNePal(X))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
ACTIVE(isNePal(X)) → ACTIVE(X)
ACTIVE(and(X1, X2)) → ACTIVE(X1)
ACTIVE(__(X1, X2)) → ACTIVE(X2)
ACTIVE(__(X1, X2)) → ACTIVE(X1)
The value of delta used in the strict ordering is 8.
POL(__(x1, x2)) = 2 + (4)x_1 + x_2
POL(isNePal(x1)) = 3 + x_1
POL(and(x1, x2)) = 4 + (2)x_1
POL(ACTIVE(x1)) = (4)x_1
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
↳ QDP
active(__(__(X, Y), Z)) → mark(__(X, __(Y, Z)))
active(__(X, nil)) → mark(X)
active(__(nil, X)) → mark(X)
active(and(tt, X)) → mark(X)
active(isNePal(__(I, __(P, I)))) → mark(tt)
active(__(X1, X2)) → __(active(X1), X2)
active(__(X1, X2)) → __(X1, active(X2))
active(and(X1, X2)) → and(active(X1), X2)
active(isNePal(X)) → isNePal(active(X))
__(mark(X1), X2) → mark(__(X1, X2))
__(X1, mark(X2)) → mark(__(X1, X2))
and(mark(X1), X2) → mark(and(X1, X2))
isNePal(mark(X)) → mark(isNePal(X))
proper(__(X1, X2)) → __(proper(X1), proper(X2))
proper(nil) → ok(nil)
proper(and(X1, X2)) → and(proper(X1), proper(X2))
proper(tt) → ok(tt)
proper(isNePal(X)) → isNePal(proper(X))
__(ok(X1), ok(X2)) → ok(__(X1, X2))
and(ok(X1), ok(X2)) → ok(and(X1, X2))
isNePal(ok(X)) → ok(isNePal(X))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPOrderProof
TOP(mark(X)) → TOP(proper(X))
TOP(ok(X)) → TOP(active(X))
active(__(__(X, Y), Z)) → mark(__(X, __(Y, Z)))
active(__(X, nil)) → mark(X)
active(__(nil, X)) → mark(X)
active(and(tt, X)) → mark(X)
active(isNePal(__(I, __(P, I)))) → mark(tt)
active(__(X1, X2)) → __(active(X1), X2)
active(__(X1, X2)) → __(X1, active(X2))
active(and(X1, X2)) → and(active(X1), X2)
active(isNePal(X)) → isNePal(active(X))
__(mark(X1), X2) → mark(__(X1, X2))
__(X1, mark(X2)) → mark(__(X1, X2))
and(mark(X1), X2) → mark(and(X1, X2))
isNePal(mark(X)) → mark(isNePal(X))
proper(__(X1, X2)) → __(proper(X1), proper(X2))
proper(nil) → ok(nil)
proper(and(X1, X2)) → and(proper(X1), proper(X2))
proper(tt) → ok(tt)
proper(isNePal(X)) → isNePal(proper(X))
__(ok(X1), ok(X2)) → ok(__(X1, X2))
and(ok(X1), ok(X2)) → ok(and(X1, X2))
isNePal(ok(X)) → ok(isNePal(X))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
TOP(mark(X)) → TOP(proper(X))
Used ordering: Polynomial interpretation [25,35]:
TOP(ok(X)) → TOP(active(X))
The value of delta used in the strict ordering is 1/16.
POL(active(x1)) = x_1
POL(__(x1, x2)) = 1/2 + (4)x_1 + x_2
POL(tt) = 0
POL(mark(x1)) = 1/4 + x_1
POL(ok(x1)) = x_1
POL(TOP(x1)) = (1/4)x_1
POL(isNePal(x1)) = 1/2 + x_1
POL(proper(x1)) = x_1
POL(and(x1, x2)) = 3/4 + (13/4)x_1 + (4)x_2
POL(nil) = 0
active(isNePal(__(I, __(P, I)))) → mark(tt)
active(__(X1, X2)) → __(active(X1), X2)
active(__(nil, X)) → mark(X)
active(and(tt, X)) → mark(X)
active(isNePal(X)) → isNePal(active(X))
__(mark(X1), X2) → mark(__(X1, X2))
active(__(X1, X2)) → __(X1, active(X2))
active(and(X1, X2)) → and(active(X1), X2)
isNePal(mark(X)) → mark(isNePal(X))
proper(__(X1, X2)) → __(proper(X1), proper(X2))
__(X1, mark(X2)) → mark(__(X1, X2))
and(mark(X1), X2) → mark(and(X1, X2))
proper(tt) → ok(tt)
proper(isNePal(X)) → isNePal(proper(X))
proper(nil) → ok(nil)
proper(and(X1, X2)) → and(proper(X1), proper(X2))
isNePal(ok(X)) → ok(isNePal(X))
and(ok(X1), ok(X2)) → ok(and(X1, X2))
__(ok(X1), ok(X2)) → ok(__(X1, X2))
active(__(X, nil)) → mark(X)
active(__(__(X, Y), Z)) → mark(__(X, __(Y, Z)))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDPOrderProof
TOP(ok(X)) → TOP(active(X))
active(__(__(X, Y), Z)) → mark(__(X, __(Y, Z)))
active(__(X, nil)) → mark(X)
active(__(nil, X)) → mark(X)
active(and(tt, X)) → mark(X)
active(isNePal(__(I, __(P, I)))) → mark(tt)
active(__(X1, X2)) → __(active(X1), X2)
active(__(X1, X2)) → __(X1, active(X2))
active(and(X1, X2)) → and(active(X1), X2)
active(isNePal(X)) → isNePal(active(X))
__(mark(X1), X2) → mark(__(X1, X2))
__(X1, mark(X2)) → mark(__(X1, X2))
and(mark(X1), X2) → mark(and(X1, X2))
isNePal(mark(X)) → mark(isNePal(X))
proper(__(X1, X2)) → __(proper(X1), proper(X2))
proper(nil) → ok(nil)
proper(and(X1, X2)) → and(proper(X1), proper(X2))
proper(tt) → ok(tt)
proper(isNePal(X)) → isNePal(proper(X))
__(ok(X1), ok(X2)) → ok(__(X1, X2))
and(ok(X1), ok(X2)) → ok(and(X1, X2))
isNePal(ok(X)) → ok(isNePal(X))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
TOP(ok(X)) → TOP(active(X))
The value of delta used in the strict ordering is 1/8.
POL(active(x1)) = x_1
POL(__(x1, x2)) = 4 + (3)x_1 + (1/2)x_2
POL(tt) = 1/4
POL(ok(x1)) = 1/2 + x_1
POL(mark(x1)) = 1/2 + (1/4)x_1
POL(TOP(x1)) = (1/4)x_1
POL(isNePal(x1)) = (4)x_1
POL(and(x1, x2)) = 3/4 + x_2
POL(nil) = 0
active(isNePal(__(I, __(P, I)))) → mark(tt)
active(__(X1, X2)) → __(active(X1), X2)
active(__(nil, X)) → mark(X)
active(and(tt, X)) → mark(X)
active(isNePal(X)) → isNePal(active(X))
__(mark(X1), X2) → mark(__(X1, X2))
active(__(X1, X2)) → __(X1, active(X2))
active(and(X1, X2)) → and(active(X1), X2)
isNePal(mark(X)) → mark(isNePal(X))
__(X1, mark(X2)) → mark(__(X1, X2))
and(mark(X1), X2) → mark(and(X1, X2))
isNePal(ok(X)) → ok(isNePal(X))
and(ok(X1), ok(X2)) → ok(and(X1, X2))
__(ok(X1), ok(X2)) → ok(__(X1, X2))
active(__(X, nil)) → mark(X)
active(__(__(X, Y), Z)) → mark(__(X, __(Y, Z)))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
active(__(__(X, Y), Z)) → mark(__(X, __(Y, Z)))
active(__(X, nil)) → mark(X)
active(__(nil, X)) → mark(X)
active(and(tt, X)) → mark(X)
active(isNePal(__(I, __(P, I)))) → mark(tt)
active(__(X1, X2)) → __(active(X1), X2)
active(__(X1, X2)) → __(X1, active(X2))
active(and(X1, X2)) → and(active(X1), X2)
active(isNePal(X)) → isNePal(active(X))
__(mark(X1), X2) → mark(__(X1, X2))
__(X1, mark(X2)) → mark(__(X1, X2))
and(mark(X1), X2) → mark(and(X1, X2))
isNePal(mark(X)) → mark(isNePal(X))
proper(__(X1, X2)) → __(proper(X1), proper(X2))
proper(nil) → ok(nil)
proper(and(X1, X2)) → and(proper(X1), proper(X2))
proper(tt) → ok(tt)
proper(isNePal(X)) → isNePal(proper(X))
__(ok(X1), ok(X2)) → ok(__(X1, X2))
and(ok(X1), ok(X2)) → ok(and(X1, X2))
isNePal(ok(X)) → ok(isNePal(X))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))